g:IMonoid, p, q:, E:({p..q}|g|). ( p  i < q. E(i))  |g| 

latex

Up	groups 1
Definitions of Statement	IMonoid,  lb  i < ub. E(i)
Definitions	x. t(x), x(s),  lb  i < ub. E(i), t  T, x:A. B(x), IMonoid
Lemmas	imon wf, int seg wf, grp id wf, grp op wf, grp car wf, itop wf